$\forall$$T$, ${\it T'}$:Type, $f$:($T$$\rightarrow$${\it T'}$), $L$:$T$ List, ${\it x'}$, ${\it y'}$:${\it T'}$.
\\[0ex]${\it x'}$ before ${\it y'}$ $\in$ map($f$;$L$) $\Leftrightarrow$ ($\exists$$x$, $y$:$T$. $x$ before $y$ $\in$ $L$ \& $f$($x$) $=$ ${\it x'}$ \& $f$($y$) $=$ ${\it y'}$)